Automata-Driven Automated Induction
Identifieur interne : 00BA10 ( Main/Exploration ); précédent : 00BA09; suivant : 00BA11Automata-Driven Automated Induction
Auteurs : Adel Bouhoula ; Jean-Pierre JouannaudSource :
English descriptors
Abstract
This work investigates inductive theorem proving techniques for first-order functions whose meaning and domains can be specified by Horn Clauses built up from the equality and finitely many unary membership predicates. In contrast with other works in the area, constructors are not assumed to be free. Techniques originating from tree automata are used to describe ground constructor terms in normal form, on which the induction proofs are built up. Validity of (free) constructor clauses is checked by an original technique relying on the recent discovery of a complete axiomatisation of finite trees and their rational subsets. Validity of clauses with defined symbols or non-free constructor terms is reduced to the latter case by appropriate inference rules using a notion of ground reducibility for these symbols. We show how to check this property by generating proof obligations which can be passed over to the inductive prover.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 001F88
- to stream Crin, to step Curation: 001F88
- to stream Crin, to step Checkpoint: 002733
- to stream Main, to step Merge: 00C187
- to stream Main, to step Curation: 00BA10
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="261">Automata-Driven Automated Induction</title></titleStmt><publicationStmt><idno type="RBID">CRIN:bouhoula97b</idno><date when="1997" year="1997">1997</date><idno type="wicri:Area/Crin/Corpus">001F88</idno><idno type="wicri:Area/Crin/Curation">001F88</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001F88</idno><idno type="wicri:Area/Crin/Checkpoint">002733</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">002733</idno><idno type="wicri:Area/Main/Merge">00C187</idno><idno type="wicri:Area/Main/Curation">00BA10</idno><idno type="wicri:Area/Main/Exploration">00BA10</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Automata-Driven Automated Induction</title><author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name></author><author><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Inductive Theorem Proving</term><term>Tree Automata Techniques</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2891">This work investigates inductive theorem proving techniques for first-order functions whose meaning and domains can be specified by Horn Clauses built up from the equality and finitely many unary membership predicates. In contrast with other works in the area, constructors are not assumed to be free. Techniques originating from tree automata are used to describe ground constructor terms in normal form, on which the induction proofs are built up. Validity of (free) constructor clauses is checked by an original technique relying on the recent discovery of a complete axiomatisation of finite trees and their rational subsets. Validity of clauses with defined symbols or non-free constructor terms is reduced to the latter case by appropriate inference rules using a notion of ground reducibility for these symbols. We show how to check this property by generating proof obligations which can be passed over to the inductive prover.</div></front></TEI><affiliations><list></list><tree><noCountry><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name><name sortKey="Jouannaud, Jean Pierre" sort="Jouannaud, Jean Pierre" uniqKey="Jouannaud J" first="Jean-Pierre" last="Jouannaud">Jean-Pierre Jouannaud</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00BA10 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00BA10 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:bouhoula97b
|texte= Automata-Driven Automated Induction
}}
| This area was generated with Dilib version V0.6.33. |  |